The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0, x2) → x2
drop#2(S(0), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0, x2) → Nil
take#2(S(0), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0) → 0
halve#1(S(0)) → S(0)
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0, x16) → True
leq#2(S(x20), 0) → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, Cons(0, x669746_11), x2, x1) →⁺ Cons(x4, cond_merge_ys_zs_2(True, Cons(0, x669746_11), Cons(x5, x6), 0, x669746_11, x5, x6))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x669746_11 / Cons(0, x669746_11)].
The result substitution is [x7 / 0, x8 / x669746_11, x4 / 0, x2 / x5, x1 / x6].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(Cons(x51, Cons(x25, x33)), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(x3, Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

S is empty.
Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
const_f#2/0

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

S is empty.
Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
take#2, drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(10) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
take#2, drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol take#2.

(12) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
drop#2, merge#2, leq#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol drop#2.

(14) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
leq#2, merge#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
leq#2 < merge#2
halve#1 < map#2
length#1 < map#2

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol leq#2.

(16) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
merge#2, map#2, halve#1, length#1

They will be analysed ascendingly in the following order:
halve#1 < map#2
length#1 < map#2

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol merge#2.

(18) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
halve#1, map#2, length#1

They will be analysed ascendingly in the following order:
halve#1 < map#2
length#1 < map#2

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol halve#1.

(20) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
length#1, map#2

They will be analysed ascendingly in the following order:
length#1 < map#2

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

Induction Base:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, 0)))

Induction Step:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, +(n746_11, 1)))) →_R^Ω(1)
S(length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11)))) →_IH
S(*10_11)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(22) Complex Obligation (BEST)

(23) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

The following defined symbols remain to be analysed:
map#2

(24) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11), rt ∈ Ω(1 + n1214₁₁)

Induction Base:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0)) →_R^Ω(1)
Nil

Induction Step:
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(n1214_11, 1))) →_R^Ω(1)
Cons(dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil), map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11))) →_R^Ω(1)
Cons(Nil, map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11))) →_IH
Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(c1215_11))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(25) Complex Obligation (BEST)

(26) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11), rt ∈ Ω(1 + n1214₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)
map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11)) → gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(n1214_11), rt ∈ Ω(1 + n1214₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Innermost TRS:
Rules:
divide_ys#1(x2, x1) → Cons(take#2(x1, x2), Cons(drop#2(x1, x2), Nil))
cond_merge_ys_zs_2(True, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x4, merge#2(x3, Cons(x5, x6)))
cond_merge_ys_zs_2(False, Cons(x7, x8), Cons(x5, x6), x4, x3, x2, x1) → Cons(x2, merge#2(Cons(x7, x8), x1))
merge#2(Nil, x2) → x2
merge#2(Cons(x4, x2), Nil) → Cons(x4, x2)
merge#2(Cons(x8, x6), Cons(x4, x2)) → cond_merge_ys_zs_2(leq#2(x8, x4), Cons(x8, x6), Cons(x4, x2), x8, x6, x4, x2)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Nil) → Nil
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x229, Nil)) → Cons(x229, Nil)
dc#1(map, divisible, mergesort_zs_3, divide, const_f, Cons(x51, Cons(x25, x33))) → const_f#2(map#2(dc(map, divisible, mergesort_zs_3, divide, const_f), divide_ys#1(Cons(x51, Cons(x25, x33)), S(halve#1(length#1(x33))))))
drop#2(0', x2) → x2
drop#2(S(0'), Nil) → bot[1]
drop#2(S(x10), Cons(x56, x64)) → drop#2(x10, x64)
take#2(0', x2) → Nil
take#2(S(0'), Nil) → Cons(bot[0], Nil)
take#2(S(x22), Cons(x56, x64)) → Cons(x56, take#2(x22, x64))
halve#1(0') → 0'
halve#1(S(0')) → S(0')
halve#1(S(S(x14))) → S(halve#1(x14))
const_f#2(Cons(x6, Cons(x4, x2))) → merge#2(x6, x4)
leq#2(0', x16) → True
leq#2(S(x20), 0') → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
length#1(Nil) → 0'
length#1(Cons(x6, x8)) → S(length#1(x8))
map#2(dc(x2, x4, x6, x8, x10), Nil) → Nil
map#2(dc(x6, x8, x10, x12, x14), Cons(x4, x2)) → Cons(dc#1(x6, x8, x10, x12, x14, x4), map#2(dc(x6, x8, x10, x12, x14), x2))
main(x113) → dc#1(map, divisible, mergesort_zs_3, divide, const_f, x113)

Types:
divide_ys#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Cons :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
take#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
drop#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
Nil :: Nil:Cons:S:0':bot[1]:bot[0]
cond_merge_ys_zs_2 :: True:False → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
True :: True:False
merge#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
False :: True:False
leq#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0] → True:False
dc#1 :: map → divisible → mergesort_zs_3 → divide → const_f → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map :: map
divisible :: divisible
mergesort_zs_3 :: mergesort_zs_3
divide :: divide
const_f :: const_f
const_f#2 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
map#2 :: dc → Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
dc :: map → divisible → mergesort_zs_3 → divide → const_f → dc
S :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
halve#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
length#1 :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
0' :: Nil:Cons:S:0':bot[1]:bot[0]
bot[1] :: Nil:Cons:S:0':bot[1]:bot[0]
bot[0] :: Nil:Cons:S:0':bot[1]:bot[0]
main :: Nil:Cons:S:0':bot[1]:bot[0] → Nil:Cons:S:0':bot[1]:bot[0]
hole_Nil:Cons:S:0':bot[1]:bot[0]1_11 :: Nil:Cons:S:0':bot[1]:bot[0]
hole_True:False2_11 :: True:False
hole_map3_11 :: map
hole_divisible4_11 :: divisible
hole_mergesort_zs_35_11 :: mergesort_zs_3
hole_divide6_11 :: divide
hole_const_f7_11 :: const_f
hole_dc8_11 :: dc
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11 :: Nat → Nil:Cons:S:0':bot[1]:bot[0]

Lemmas:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

Generator Equations:
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(0) ⇔ Nil
gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(x, 1)) ⇔ Cons(Nil, gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
length#1(gen_Nil:Cons:S:0':bot[1]:bot[0]9_11(+(1, n746_11))) → *10_11, rt ∈ Ω(n746₁₁)

(34) BOUNDS(n^1, INF)